1. Field of the Invention
The present invention generally relates to the field of information processing and artificial intelligence and, more particularly, to a method and an apparatus of automated theorem proving for solving a decision problem in which a provability of a proposition concerning relationships defined among physical objects is automatically judged on a basis of a given set of knowledge of the physical objects.
2. Description of the Background Art
Recent progress in computer science prompted the research and advance of a so called `knowledge processing`. In this type of information processing, a language called `Prolog` is often employed, which incorporates a mechanism for an answer to a posed question to be automatically sought on a basis of, and derived, if possible, from a prescribed set of knowledge. As can be found in detail in `Programming in Prolog`, Springer-Verlag, 1981, by W. F. Clocksin and C. S. Mellish (this will be referred hereafter as Ref. 1), in Prolog, knowledge given in the form of "clause" (a precise definition of this and other technical terms will be given below) will be regarded as an axiom and a question posed also in a form of clause will be regarded as a theorem to be proved.
Although technique of automated theorem proving is mostly utilized in the field of such an knowledge processing, it is also highly useful in the automatic validation of programs and logical circuits.
Details of the conventional technique of automated theorem proving can be found in `Symbolic Logic and Mechanical Theorem Proving`, Academic Press, 1973, by Chin-Liang Chang and Richard Char-Tung Lee (this will be referred hereafter as Ref. 2). Some basic facts and relevant conventional technique which can be found in this Ref. 2 will be described in some detail below in the DETAILED DESCRIPTION OF THE PREFERRED EMBODIMENTS in relations to the present invention. Here, without giving any definitions to terms, the problems of the prior art will be summarized.
In automated theorem proving, in essence, the problem of theorem proving is dealt with by transforming the problem into an equivalent problem of determining the unsatisfiability of the set of clauses, on a basis of the fact that "If a given theorem can be proved on a basis of the axioms (i.e., if a given theorem is true), then a set of clauses obtained by adding a clause representing a negation of the given theorem to a set of clauses of the axioms is unsatisfiable". That a set of clauses is satisfiable means there exists an "allotting (or interpretation)" of logical values under which all the clauses in the set of clauses can simultaneously be "true".
For the determination of the unsatisfiability of the set of clauses, a technique called the "resolution principle" has conventionally been used. The "resolution" is a kind of deduction in which a clause called a "resolvent" is derived from two clauses, which resolvent is guaranteed to be true when two original clauses are true. The unsatisfiability of the set of clauses is determined on a basis of the fact that "If a set of clauses is unsatisfiable, then it is possible to derive an `empty clause` from this set of clauses by repeating the resolution" (the fact known as the "completeness of the resolution" principle).
Thus, conventionally, how fast can the empty clause be derived by repeating the resolution, or alternatively, how fast can the fact that an empty clause cannot be derived be shown, has been critical issues.
Now, for the resolution to be able to derive a resolvent, it is necessary that one and the other of the two original clauses contains one and the other member of a complementary pair (a possible) complementary pair, to be exact), respectively. Consequently, in order to derive an empty clause by the resolution, it is necessary at each step of resolution (1) to find quickly a pair of clauses for which one and the other of the pair contains one and the other member of a complementary pair, respectively, and (2) to guess one pair among all such pairs from which the empty clause can be derived faster than from the other pair.
To this end, various techniques, such as a unit resolution, a linear resolution, and lock resolution have been developed. However, these conventional techniques share in common a drawback that their efficiency (i.e., speed of deriving the empty clause) varies for different clauses to be dealt with, and that when no empty clause can be derived (i.e., when the clause is satisfiable) all the possible resolutions will be attempted, so that the efficiency is very low for such a case.
Furthermore, conventionally, the very nature of techniques using the resolution defied a realization of parallel processing to perform them at high-speed.